(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(assert v1)
(declare-const _13-0 (_ BitVec 13))
(assert v6)
(assert v12)
(assert (and v9 (=> v10 v1) v1 v4 v9 v6 v12 v10))
(declare-const _29-0 (_ BitVec 29))
(assert (=> (= #b0101001111 #b0101001111) (bvule #b0101001111 #b0101001111)))
(assert (and v9 (=> v10 v1) v1 v4 v9 v6 v12 v10))
(declare-const v13 Bool)
(assert (not (distinct v8 (not v7) v10 v8 v10 (= #b0101001111 #b0101001111) v5)))
(declare-const v14 Bool)
(assert (=> v11 v3))
(declare-const v15 Bool)
(declare-const v16 Bool)
(assert (= v13 (=> v11 v3) (not (distinct v8 (not v7) v10 v8 v10 (= #b0101001111 #b0101001111) v5)) v5 v14 (= (bvsdiv _13-0 _13-0) _13-0) v8))
(check-sat)
